We introduce the class of rational Kripke models and study symbolic modelchecking of the basic tense logic Kt and some extensions of it in models fromthat class. Rational Kripke models are based on (generally infinite) rationalgraphs, with vertices labeled by the words in some regular language andtransitions recognized by asynchronous two-head finite automata, also known asrational transducers. Every atomic proposition in a rational Kripke model isevaluated in a regular set of states. We show that every formula of Kt has aneffectively computable regular extension in every rational Kripke model, andtherefore local model checking and global model checking of Kt in rationalKripke models are decidable. These results are lifted to a number of extensionsof Kt. We study and partly determine the complexity of the model checkingprocedures.
展开▼
